Tools for creating valid system designs and implementations
By "valid system designs and implemetations", we mean designs and systems that satisfy their requirements. The tools creating such systems can be classified into the following categories:
- Program Proving: The earliest efforts have been aimed at building program proving tools that check whether a given program satisfies its requirements which may be defined in terms of input and output assertions, invariants, etc. Such tools are based on theorem proving: The axioms related to the semantics of the programming language and the structure of the given program give rise to a large number of propositions, and the theorem proving tool is used to prove that the requirements are implied by these propositions. Theorem proving is an undecidable problem, therefore this approach cannot be completely automated (there exist no algorithm for theorem proving). As a consequence, one has to use human-assisted theorem provers to implement this approach. - It is difficult to perform in most cases.
- Model Checking: For state machines, there exist an algorithm (called Model Checking), that checks whether a given state machine satisfies properties that are defined in terms of temporal logic. Many tools for automatic model checking have been developed. For distributed systems, model checking of global requirements defined in terms of a temporal logic property must be preceeded by reachability analysis in order to obtain a global system model. Therefore most model checking tools include also the reachability analysis function. In the case of on-the-fly analysis, the global system model is not explicitely generated, but it is explored "on the fly" and at the same time the temporal logic requirements are checked.
- Model checking for extended state machine models has also been developed, and programs can be interpreted as extended state machines - thus model checking for programs is also possible.
- Synthesis: While in the above two approaches, the designer has to develop the design for a given requirements definition and can use the tools for checking that his design is valid. With the synthesis approach, a valid design is automatically generated from the given requirements. In general, this problem is also undecidable - therefore there exist no algorithm for doing this in general, but for certain important cases, synthesis algorithm exist, such as the following:
- Synthesizing a state machine that satisfies a given temporal logic property.
- Control theory: For a given behavior of a plant, given input from the environment and given behavior objective for the plant, it is possible to synthesize the behavior of a controller that will retrain the behavior of the plant in such a way that the behavior objective will be satisfied by the plant (if this is possible). Note that some interactions of the plant may not be visible by the controller, and some of the visible interactions may not be controllable (constrainable) by the controller.
- Protocol derivation from service specification: Given a global behavior (service specification) which defines actions for different components in a distributed environment, and assuming reliable message transfer between the different components, one can automatically derive the specification of a protocol to be executed by the different components which assures that the actions of the global behavior are performed in an order that satisfies the global service specification. For details, see next chapter of this course
Suggested tools
- This
is an interesting tool for verifying properties of distributed systems. It
uses the Promela language (related to C; with concurrent processes and queue communication) for the definition of the system to be analysed. It
allows the specification, in temporal logic, of properties to be
verified. This is based on relatively exhaustive state space exploration. Here is a paper on Spin by its author. Here is a tutorial.
CPN - a tool for modeling with Colored Petri Nets (see also Petri Nets World)
- This tool supports extended Petri nets (with tokens containing attributes - colors). See example simple_protocol
LTSA - Labelled Transition System Analyser (see overview of LTSA)
Alloy - a tool based on first-order logic
using an object-oriented syntax - for describing and analysing the structure and the behavior of systems
- The described objects may represent temporal states of a dynamic system;
therefore the system may be used for describing the possible sequences of
states during the execution of a system.
- System properties may be specified by assertions. These assertions can
be checked during the analysis for "all" system configurations that can be
built according to the specification ("all" within some
artificial limit imposed by the designer - in order to avoid the exploration
of an infinite number of possibilities). You may down-load the tool.
- Read (and try) for instance the Tutorial - chapter 2 (River Crossing)
UPPAAL - a tool for modeling extended state machine models possibly including hard real-time constraints (Timed Automata) - have look at the demos that come with the tool.
- Under "Support" you can find Help pages, an overview, a tutorial text presenting UPPAAL with a detailed example, introductory Powerpoint slides - Also look at the demo examples included in the tool: fischer (a time-based mutual exclusion algorithm) and train_gate
- You can down-load the tool; note that there is an academic version. Use the command File -> Open System to open some demos that come with the tool. Look at the train-gate, in particular.
- Note: The interactions in UPPAAL are inputs or outputs (like in IOA), but the communication semantics for communicating components is by rendezvous (the semantics of UPPAAL is based on LTS with added timers).
- Branching-time temporal logic can be used to defined abstract behavior properties
Other specification methods and tools
UML State Machines - see here
First-order logic - theorem prover for Z (not suggested for a project)
- The theorem prover, called Z/EVES, from ORA Canada can be obtained without charge (at
least this was the case in 2003). It supports Z as the language for writing the system
specification and the properties to be proven. From what I have heard about
it, it was an interesting system, but it is not available any more from the creators.
IOAutomata (for applications of the controller derivation algorithm - not covered in this course in 2013)
- Drissi's tool is described in this
paper . The construction algorithm implemented in this tool is described
in more details here .
Requirements capture tool for Live Sequence Charts (LSC)
- LSC is a kind of improved version of Message Sequence Charts. This tool
lets the user "play in" sequences of system interactions (inputs and
corresponding expected outputs) and later allows to "play out" the captured
requirements while the user only provides inputs and the tool produces the
required outputs of the system. (I have not tried it out)
Deriving MSCs (or UML sequence diagrams) from User Case Maps
- The latest version of the UCM Navigator also supports the generation of MSCs from a given UCM by
letting the user select the possible choice at branching points. Currently,
however, the generated MSCs can be displayed, but are not compatible for
input to other modeling tools, such as the Telelogic SDL tool..
Created: November 6, 2014